ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;A + Top), es:ES.
es-decl(es;ds;da)  ([[interface-left(X)]] = es-interface-left([[X]])  AbsInterface(A)) 

latex

Definitions

Knd, Id, Type, Interface(ds;da;A), ES, es-decl(es;ds;da), <a, b>, f(a), P  Q, interface-left(X), x:A. B(x), s = t, es-interface-left(X), [[X]], t  T, x:AB(x), left + right, Top, E, AbsInterface(A), s ~ t, in-interface(es;X;e), f o g  , can-apply(f;x), do-apply(f;x), fpf dom compose compseq tag def, Unit, P  Q, P & Q, , if b then t else f fi , fpf ap compose compseq tag def, interface-val(es;X;e), ff, A, False, t.1, b, x:A  B(x), a:A fp B(a)

Lemmas

assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-interface-left wf, abs-interface wf